(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 109))
(declare-fun v1 () (_ BitVec 16))
(declare-fun v2 () (_ BitVec 9))
(declare-fun v3 () (_ BitVec 71))
(assert (let ((e4(_ bv671259241189034709885216 80)))
(let ((e5(_ bv15622996484789540157023977446 94)))
(let ((e6 (bvneg v0)))
(let ((e7 (bvshl e6 v0)))
(let ((e8 (ite (bvule v3 v3) (_ bv1 1) (_ bv0 1))))
(let ((e9 (ite (bvslt ((_ sign_extend 93) e8) e5) (_ bv1 1) (_ bv0 1))))
(let ((e10 (bvneg e4)))
(let ((e11 (bvsdiv e7 e7)))
(let ((e12 (ite (= ((_ sign_extend 55) v1) v3) (_ bv1 1) (_ bv0 1))))
(let ((e13 (bvxor e4 e4)))
(let ((e14 ((_ sign_extend 0) e6)))
(let ((e15 (bvcomp ((_ zero_extend 108) e12) e7)))
(let ((e16 (bvand ((_ sign_extend 79) e8) e13)))
(let ((e17 (bvsdiv ((_ zero_extend 108) e12) e7)))
(let ((e18 ((_ rotate_right 95) e17)))
(let ((e19 ((_ extract 11 9) e14)))
(let ((e20 (bvxnor ((_ zero_extend 79) e8) e16)))
(let ((e21 (bvlshr e20 e16)))
(let ((e22 (bvmul ((_ zero_extend 29) e16) v0)))
(let ((e23 ((_ sign_extend 37) e13)))
(let ((e24 ((_ sign_extend 14) e17)))
(let ((e25 (concat v2 e19)))
(let ((e26 (bvult ((_ sign_extend 79) e8) e21)))
(let ((e27 (bvugt e6 ((_ zero_extend 29) e21))))
(let ((e28 (bvugt e5 ((_ zero_extend 14) e16))))
(let ((e29 (distinct e18 ((_ zero_extend 29) e20))))
(let ((e30 (bvsge v2 ((_ sign_extend 6) e19))))
(let ((e31 (= ((_ zero_extend 108) e15) e7)))
(let ((e32 (bvult ((_ sign_extend 29) e20) e6)))
(let ((e33 (bvsle e18 ((_ sign_extend 29) e4))))
(let ((e34 (bvsgt ((_ zero_extend 64) v1) e20)))
(let ((e35 (distinct ((_ zero_extend 100) v2) e18)))
(let ((e36 (bvsle e4 ((_ zero_extend 79) e8))))
(let ((e37 (distinct ((_ zero_extend 38) v3) e7)))
(let ((e38 (bvslt e18 ((_ sign_extend 108) e8))))
(let ((e39 (bvsgt ((_ sign_extend 108) e8) e7)))
(let ((e40 (bvsge ((_ sign_extend 108) e15) e11)))
(let ((e41 (distinct e5 ((_ zero_extend 14) e10))))
(let ((e42 (= e18 ((_ zero_extend 15) e5))))
(let ((e43 (bvsgt ((_ sign_extend 43) e16) e24)))
(let ((e44 (bvugt ((_ sign_extend 59) e25) v3)))
(let ((e45 (distinct ((_ sign_extend 93) v1) e22)))
(let ((e46 (bvsle ((_ sign_extend 29) e10) e17)))
(let ((e47 (bvslt v2 v2)))
(let ((e48 (distinct ((_ zero_extend 82) e25) e5)))
(let ((e49 (bvsgt ((_ sign_extend 43) e20) e24)))
(let ((e50 (= ((_ sign_extend 79) e15) e10)))
(let ((e51 (bvsgt e7 ((_ sign_extend 93) v1))))
(let ((e52 (bvsge ((_ sign_extend 14) e13) e5)))
(let ((e53 (bvsle e16 e20)))
(let ((e54 (bvuge e17 e6)))
(let ((e55 (bvugt ((_ sign_extend 15) e5) e11)))
(let ((e56 (bvsle ((_ zero_extend 106) e19) e14)))
(let ((e57 (bvslt v2 ((_ zero_extend 8) e8))))
(let ((e58 (bvsgt ((_ sign_extend 29) e20) e17)))
(let ((e59 (bvsgt ((_ zero_extend 71) v2) e13)))
(let ((e60 (bvsgt ((_ zero_extend 108) v2) e23)))
(let ((e61 (= e16 ((_ sign_extend 9) v3))))
(let ((e62 (distinct ((_ sign_extend 106) e19) e11)))
(let ((e63 (distinct ((_ zero_extend 29) e13) e17)))
(let ((e64 (bvslt ((_ zero_extend 29) e4) e22)))
(let ((e65 (bvult e16 ((_ zero_extend 71) v2))))
(let ((e66 (bvsle e20 ((_ zero_extend 9) v3))))
(let ((e67 (bvsgt e13 ((_ zero_extend 9) v3))))
(let ((e68 (bvsle ((_ sign_extend 68) e25) e21)))
(let ((e69 (bvugt e14 ((_ sign_extend 108) e12))))
(let ((e70 (bvslt e16 ((_ zero_extend 77) e19))))
(let ((e71 (bvult e11 ((_ zero_extend 15) e5))))
(let ((e72 (= ((_ sign_extend 79) e15) e4)))
(let ((e73 (bvult ((_ zero_extend 14) e6) e24)))
(let ((e74 (bvsle ((_ zero_extend 108) e8) e22)))
(let ((e75 (bvsle ((_ zero_extend 38) v3) e17)))
(let ((e76 (bvslt e20 ((_ zero_extend 79) e9))))
(let ((e77 (bvsgt e11 ((_ sign_extend 108) e15))))
(let ((e78 (bvugt e14 ((_ zero_extend 93) v1))))
(let ((e79 (bvuge v0 ((_ zero_extend 108) e12))))
(let ((e80 (not e69)))
(let ((e81 (=> e71 e39)))
(let ((e82 (not e43)))
(let ((e83 (not e40)))
(let ((e84 (or e45 e28)))
(let ((e85 (=> e83 e53)))
(let ((e86 (=> e74 e37)))
(let ((e87 (ite e82 e68 e63)))
(let ((e88 (xor e36 e52)))
(let ((e89 (xor e87 e46)))
(let ((e90 (or e70 e34)))
(let ((e91 (=> e30 e60)))
(let ((e92 (or e66 e89)))
(let ((e93 (or e75 e44)))
(let ((e94 (not e55)))
(let ((e95 (ite e90 e33 e54)))
(let ((e96 (= e59 e61)))
(let ((e97 (=> e62 e26)))
(let ((e98 (= e94 e85)))
(let ((e99 (= e86 e73)))
(let ((e100 (ite e57 e48 e64)))
(let ((e101 (ite e80 e81 e65)))
(let ((e102 (and e100 e72)))
(let ((e103 (= e79 e56)))
(let ((e104 (xor e88 e29)))
(let ((e105 (ite e101 e95 e77)))
(let ((e106 (xor e96 e103)))
(let ((e107 (=> e49 e31)))
(let ((e108 (=> e27 e32)))
(let ((e109 (xor e91 e76)))
(let ((e110 (=> e38 e42)))
(let ((e111 (ite e109 e99 e41)))
(let ((e112 (=> e98 e108)))
(let ((e113 (not e105)))
(let ((e114 (xor e111 e51)))
(let ((e115 (= e106 e102)))
(let ((e116 (=> e114 e97)))
(let ((e117 (=> e35 e92)))
(let ((e118 (and e117 e67)))
(let ((e119 (=> e110 e110)))
(let ((e120 (ite e118 e115 e50)))
(let ((e121 (and e119 e116)))
(let ((e122 (not e120)))
(let ((e123 (and e93 e78)))
(let ((e124 (not e47)))
(let ((e125 (and e113 e107)))
(let ((e126 (xor e84 e58)))
(let ((e127 (=> e104 e126)))
(let ((e128 (ite e127 e121 e125)))
(let ((e129 (or e124 e128)))
(let ((e130 (not e123)))
(let ((e131 (= e112 e122)))
(let ((e132 (or e131 e130)))
(let ((e133 (or e129 e132)))
(let ((e134 (and e133 (not (= e7 (_ bv0 109))))))
(let ((e135 (and e134 (not (= e7 (bvnot (_ bv0 109)))))))
e135
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
